(0) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
member(x', Cons(x, xs)) → member[Ite][True][Ite](!EQ(x', x), x', Cons(x, xs))
member(x, Nil) → False
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
goal(x, xs) → member(x, xs)
The (relative) TRS S consists of the following rules:
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0, S(y)) → False
!EQ(S(x), 0) → False
!EQ(0, 0) → True
member[Ite][True][Ite](False, x', Cons(x, xs)) → member(x', xs)
member[Ite][True][Ite](True, x, xs) → True
Rewrite Strategy: INNERMOST
(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
member(0, Cons(S(y11_1), xs)) →+ member(0, xs)
gives rise to a decreasing loop by considering the right hand sides subterm at position [].
The pumping substitution is [xs / Cons(S(y11_1), xs)].
The result substitution is [ ].
(2) BOUNDS(n^1, INF)